#include <string>
#include <vector>
#include <map>
#include <list>
#include <stack>
#include <typeinfo>
using namespace std;

//Prop::= true | false | ~Prop | Prop ^ Prop | Expr v Expr | Expr == Expr
enum QuantType {Forall, Exist};
enum StmtType { st_Assign, st_Goto, st_Return, st_Label, st_FUNC_Call };
enum PropType { LT, GT, Eq};
enum LogicType { And, Or, Imp};
enum OPType { Plus, Minus, Multi, Divide };

struct Expr{// 0:Expr, 1:IntExpr, 2.ArrayExpr, 3:VarExpr, 4:BinExpr
    //int Flag;
    //virtual void member(){ };//check
    virtual ~Expr(){ }
    virtual bool operator==(Expr &other)=0;
};
struct IntExpr: Expr{//number
    int i;
    bool operator==(Expr &other);
};
struct ArrayExpr: Expr{
    char n[256];
    vector<Expr*> e;
    bool operator==(Expr &other);
};
struct VarExpr: Expr{//variable
    char x[256];
    bool operator==(Expr &other);
};
struct BinExpr: Expr{
    Expr *e1, *e2;
    OPType op;
    bool operator==(Expr &other);
};
struct Prop{
    //virtual void member(){ }
    virtual ~Prop(){ }
    virtual bool operator==(Prop &other)=0;
};
struct BoolProp:Prop{
    bool b;
    bool operator==(Prop &other);
};
struct NegProp:Prop{
    Prop *p;
    bool operator==(Prop &other);
};
struct BinProp:Prop{
    Prop *p1, *p2;
    LogicType l;
    BinProp(){}
    BinProp(Prop* p1, LogicType l, Prop* p2):p1(p1), p2(p2), l(l){}
    bool operator==(Prop &other);
};
struct InequProp:Prop{
    Expr *e1, *e2;
    PropType p;
    bool operator==(Prop &other);
};

struct QuantProp: Prop{
	Prop* p;
	char x[256];
	QuantType t;
	bool operator==(Prop &other);
};

struct Stmt{
    virtual void member(){ }
    virtual ~Stmt(){ }
};

struct Prog{
    char name[256];
    vector<VarExpr*> formal_para;
    vector<Stmt*> p;
    map<Stmt*, string> LableSet;
};



struct AssignStmt: Stmt{
    Expr *e1, *e2;
};
struct IfStmt: Stmt{
    Prop *p;
    Prog *p1, *p2;
};
struct WhileStmt:Stmt{
    Prop *p;
    Prog *p1;
};
struct AssertStmt:Stmt{
    Prop *p;
};
struct GotoStmt:Stmt{
    int type; // 1:continue, 2:break, 3:goto, 4:return
    char L[256];
    Expr *e;
};
struct LabelStmt:Stmt{
    char L[256];
};
struct CallFunStmt:Stmt{
    char fun[256];
    vector<Expr*> para;
    Expr* Ret;
};
